1. Field of the Invention
The present invention generally relates to semiconductor device designing and, in particular, to a system and method for efficiently verifying the functional equivalence between separate models of a semiconductor design.
2. Related Art
An application-specific integrated circuit (ASIC) is typically designed in stages. For example, in a first stage, a gate design may be generated that exhibits a certain logic (i.e., that produces certain output values based on the values of input signals). In a second stage, the gate design may be reshaped or condensed so that gates implementing the logic may fit onto an ASIC chip or substrate.
It is important to ensure that the logic of the gate design does not change as the designing process progresses from one stage to the next. Therefore, the design of each new stage is usually compared to the design of the previous stage to ensure that no errors were created in generating the new stage. In other words, the logic of the new stage is compared to the logic of the previous stage to ensure that the two stages are functionally equivalent.
One way to verify the functional equivalence of two stages is to compare the output generated by the new stage to the output generated by the previous stage for the same input. However, adequately testing the designs of different stages in this way usually requires the testing of a large number of states. In fact, for many large or complex ASIC circuit designs, the number of states needed to be tested is so great that the cost of equivalence checking in this way is prohibitive.
Therefore, equivalence checkers, which are usually implemented in software, have been designed that verify whether the logic of one stage matches the logic of another stage without having to compare the outputs generated by the different stages for a large number of states. The equivalence checkers build mathematical models of the ASIC design in different stages and mathematically verify that the logic implemented by two different stages are the same. The mathematical comparison of two stages to determine equivalence between the two stages is efficient and is usually the preferred way to verify functional equivalence.
In verifying the functional equivalence of the circuit designs of two different stages, conventional equivalence checkers identify mapping point pairs in the two circuit designs. Mapping point pairs, which are sometimes referred to as "cutpoints", are equivalent points that exist in both designs. For example, a point can often be identified in the design of a first stage that corresponds with a point in the design of a second stage. These corresponding points should always have the same values for a particular set of input values. These two corresponding points define a mapping point pair that can be used by equivalence checkers through techniques known in the art to verify the equivalence of the two circuit designs.
Generally, identifying mapping point pairs is the costliest step, in terms of time, performed by most conventional equivalent checkers. Therefore, the amount of time required to verify the functional equivalence of the various stages of an ASIC design can be significantly reduced if more efficient techniques for determining the mapping point pairs between the different stages are utilized.
Thus, a heretofore unaddressed need exists in the industry for providing a system and method of efficiently determining the mapping point pairs between different models of an ASIC circuit design so that the models can be efficiently checked for functional equivalence.